f, g:x:Knd fp Type, x:Knd. (x  dom(f  g))  ((x  dom(f))  (x  dom(g))) 

latex

Definitions	a:A fp B(a), x:A. B(x), x. t(x), t  T, Knd, f  g, P  Q, P & Q, P  Q, P  Q, P  Q, , b, x  dom(f), KindDeq, Top
Lemmas	fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert wf, top wf, fpf-join wf, fpf-join-dom, iff functionality wrt iff, Knd wf, fpf wf